我们为训练神经网络的时间逻辑约束提供了一种定理证明方法。我们对有限轨迹（LTL $ _F $）的线性时间逻辑的深层嵌入方式，并在Isabelle Theorem prover的高阶逻辑中表征其语义的相关评估功能。然后，我们继续正式化一个损失函数$ \ MATHCAL {l} $，我们正式证明是合理的，并且与函数$ d \ Mathcal {l} $可区分。随后，我们使用Isabelle的自动代码生成机制来生产LTL $ _F $，$ \ MATHCAL {L} $和$ D \ MATHCAL {l} $的OCAML版本，并通过Python的Ocaml绑定与Pytorch集成在一起。我们表明，当用于动态运动的现有深度学习框架中培训时，我们的方法会为常见运动规范模式（例如避免障碍和巡逻）产生预期的结果。我们方法的独特好处是完全严格的训练方法，消除了直接在诸如Python之类的“不安全”编程语言中的逻辑方面临时实施固有的许多风险。

我们在Isabelle定理箴言中展示了有限马尔可夫决定流程的正式化。我们专注于动态编程和使用加固学习代理所需的基础。特别是，我们从第一个原则（在标量和向量形式中）导出Bellman方程，导出产生任何策略P的预期值的向量计算，并继续证明存在一个普遍的最佳政策的存在折扣因子不到一个。最后，我们证明了价值迭代和策略迭代算法在有限的时间内工作，分别产生ePsilon - 最佳和完全最佳的政策。

校准仍然是脑电脑接口（BCI）中用户体验的重要问题。甚至在开始使用BCI之前，常见的实验设计往往涉及提高认知疲劳的冗长的训练期。通过依赖于先进的机器学习技术，例如转移学习，可以减少或抑制这种依赖的校准。在Riemannian BCI上建立，我们提出了一种简单有效的方案，可以在不同主题记录的数据上培训分类器，以减少校准，同时保持良好的性能。本文的主要新颖性是提出一种独特的方法，可以应用于非常不同的范式。为了展示这种方法的稳健性，我们对三个BCI范例的多个数据集进行了元分析：事件相关的电位（P300），电机图像和SSVEP。依靠MoABB开源框架来确保实验的再现性和统计分析，结果清楚地表明，该方法可以应用于任何类型的BCI范例，并且在大多数情况下都可以显着提高分级性可靠性。我们指出了一些关键特征，以进一步提高转移学习方法。

功能连接是研究大脑振荡活动的关键方法，以便为神经元相互作用的潜在动态提供重要见解，并且主要用于脑活动分析。建立脑电脑界面信息几何的进步，我们提出了一种新颖的框架，它结合了功能连接估计和基于协方差的管道来对精神状态进行分类，例如电机图像。针对每个估算器培训的riemannian分类器，并且集合分类器将决策组合在每个特征空间中。提供了对功能连接估计器的全面评估，并在不同的条件和数据集上评估最佳表演管道，称为岩酮。使用Meta分析在数据集中聚合结果，FUCONE比所有最先进的方法更好地执行。性能增益主要是对特征空间的改进的改进的改进，增加了集合分类器相对于和内部主题间变异性的鲁棒性。

对未标记的声发射（AE）数据的解释经典依赖于通用聚类方法。虽然过去已经使用了几种外部标准来选择这些算法的超参数，但很少有研究关注能够应对AE数据特异性的聚类方法中专用目标功能的发展。我们研究了如何在混合模型中，尤其是高斯混合模型（GMM）中明确表示簇的爆炸。通过修改此类模型的内部标准，我们提出了第一种聚类方法，能够通过预期最大化过程估算的参数提供有关何时发生簇的信息（ONESET），它们如何生长（动力学）及其通过它们的生长水平及其通过其激活水平时间。这种新的目标函数可容纳AE信号的连续时间戳，从而适应其发生的顺序。该方法称为GMMSEQ，经过实验验证，以表征振动下螺栓结构中的松动现象。与来自五个实验活动的原始流数据数据的三种标准聚类方法的比较表明，GMMSEQ不仅提供了有关簇时间线的有用定性信息，而且还显示出在群集表征方面更好的性能。鉴于制定开放的声学倡议并根据公平原则，数据集和代码可用于复制本文的研究。

一般照明条件中单眼图像的强大面部重建是具有挑战性的。用于使用微弱渲染的深度神经网络编码器结合的方法打开了几何，照明和反射的非常快速的单眼重建的路径。它们也可以通过自我监督的方式培训，以增加鲁棒性和更好的泛化。然而，基于光栅化的图像形成模型以及底层场景参数化，将它们限制在Lambertian的反射率和差的形状细节中。最近，在基于经典优化的框架内引入了用于单眼脸部重建的射线跟踪，并实现最先进的结果。然而，基于优化的方法本质上很慢，缺乏鲁棒性。在本文中，我们在上述方法上建立了我们的工作，并提出了一种新的方法，大大提高了一般场景中的重建质量和鲁棒性。我们通过将CNN编码器与可分散的射线示踪剂组合来实现这一点，这使得我们能够将重建基于更高级的个性化漫射和镜面，更复杂的照明模型和自阴影的合理表示。这使得即使在难以照明的场景中，也可以在重建的形状，外观和照明中进行大跃进。通过一致的面部属性重建，我们的方法导致实际应用，例如致密和自阴影去除。与最先进的方法相比，我们的结果表明了提高了方法的准确性和有效性。

Research on automated essay scoring has become increasing important because it serves as a method for evaluating students' written-responses at scale. Scalable methods for scoring written responses are needed as students migrate to online learning environments resulting in the need to evaluate large numbers of written-response assessments. The purpose of this study is to describe and evaluate three active learning methods than can be used to minimize the number of essays that must be scored by human raters while still providing the data needed to train a modern automated essay scoring system. The three active learning methods are the uncertainty-based, the topological-based, and the hybrid method. These three methods were used to select essays included as part of the Automated Student Assessment Prize competition that were then classified using a scoring model that was training with the bidirectional encoder representations from transformer language model. All three active learning methods produced strong results, with the topological-based method producing the most efficient classification. Growth rate accuracy was also evaluated. The active learning methods produced different levels of efficiency under different sample size allocations but, overall, all three methods were highly efficient and produced classifications that were similar to one another.

This paper presents a novel framework for planning in unknown and occluded urban spaces. We specifically focus on turns and intersections where occlusions significantly impact navigability. Our approach uses an inpainting model to fill in a sparse, occluded, semantic lidar point cloud and plans dynamically feasible paths for a vehicle to traverse through the open and inpainted spaces. We demonstrate our approach using a car's lidar data with real-time occlusions, and show that by inpainting occluded areas, we can plan longer paths, with more turn options compared to without inpainting; in addition, our approach more closely follows paths derived from a planner with no occlusions (called the ground truth) compared to other state of the art approaches.

Feature acquisition algorithms address the problem of acquiring informative features while balancing the costs of acquisition to improve the learning performances of ML models. Previous approaches have focused on calculating the expected utility values of features to determine the acquisition sequences. Other approaches formulated the problem as a Markov Decision Process (MDP) and applied reinforcement learning based algorithms. In comparison to previous approaches, we focus on 1) formulating the feature acquisition problem as a MDP and applying Monte Carlo Tree Search, 2) calculating the intermediary rewards for each acquisition step based on model improvements and acquisition costs and 3) simultaneously optimizing model improvement and acquisition costs with multi-objective Monte Carlo Tree Search. With Proximal Policy Optimization and Deep Q-Network algorithms as benchmark, we show the effectiveness of our proposed approach with experimental study.

The celebrated proverb that "speech is silver, silence is golden" has a long multinational history and multiple specific meanings. In written texts punctuation can in fact be considered one of its manifestations. Indeed, the virtue of effectively speaking and writing involves - often decisively - the capacity to apply the properly placed breaks. In the present study, based on a large corpus of world-famous and representative literary texts in seven major Western languages, it is shown that the distribution of intervals between consecutive punctuation marks in almost all texts can universally be characterised by only two parameters of the discrete Weibull distribution which can be given an intuitive interpretation in terms of the so-called hazard function. The values of these two parameters tend to be language-specific, however, and even appear to navigate translations. The properties of the computed hazard functions indicate that among the studied languages, English turns out to be the least constrained by the necessity to place a consecutive punctuation mark to partition a sequence of words. This may suggest that when compared to other studied languages, English is more flexible, in the sense of allowing longer uninterrupted sequences of words. Spanish reveals similar tendency to only a bit lesser extent.